\begin{tabbing}
ecl{-}trans{-}reachable(${\it ds}$;${\it da}$;$v$;$L$;$x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=let $T$,${\it ks}$,$i$,$g$,$h$,$a$,$e$ = $v$ in \+
\\[0ex]$\exists$${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List.
\\[0ex]${\it L'}$ $\leq$ $L$ $\in$ event{-}info(${\it ds}$;${\it da}$) List
\\[0ex]\& \=$\parallel$${\it L'}$$\parallel<\parallel$$L$$\parallel$\+
\\[0ex]\& \=$x$\+
\\[0ex]$=$
\\[0ex]list\_accum(\=$x$,$a$.$a$/$k$,${\it zz}$. ${\it zz}$/$s$,$v$. if deq{-}member(KindDeq;$k$;${\it ks}$)$\rightarrow$ $g$($k$,$s$,$v$,$x$) else $x$ fi;\+
\\[0ex]$i$;
\\[0ex]${\it L'}$)
\-\\[0ex]$\in$ $T$
\-\-\-
\end{tabbing}